package org.xtext.runtime.formula;

import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import org.xtext.runtime.term.ITerm;
import org.xtext.runtime.term.Variable;
import org.xtext.runtime.type.TypeException;
import org.xtext.runtime.util.Bindings;
import org.xtext.runtime.util.ILogicVisitor;


public class Predicate implements IFormula {
	public static final Predicate TRUE				= new Predicate("true", new ITerm[] {});
	public static final Predicate FALSE				= new Predicate("false", new ITerm[] {});
	
	private String identifier;
	private String signature;
	private ITerm[] terms;
	private Set<Variable> variables = new HashSet<Variable>();
	
	public Predicate() {
	}
	
	public Predicate(String identifier, ITerm[] terms) {
		this.identifier = identifier;
		this.terms = terms;
		signature = identifier + ":" + terms.length;
		
		// Extract variables from terms...
		for (ITerm term : terms) {
			if (Variable.class.isInstance(term)) {
				variables.add((Variable) term);
			}
			signature += "," + term.type().toString();
		}
	}
	
	public ITerm termAt(int index) {
		return terms[index];
	}
	
	public Set<Variable> variables() {
		return variables;
	}
	
	public int size() {
		return terms.length;
	}
	
	public String identifier() {
		return identifier;
	}
	
	public String toString() {
		String output = identifier;
		if (terms.length > 0) {
			output += "(";
			for (int i=0; i<terms.length; i++) {
				if (i > 0) output += ",";
				output += terms[i].toString();
			}
			output += ")";
		}
		return output;
	}

	public ITerm[] terms() {
		return terms;
	}

	public boolean equals(Object object) {
		if (Predicate.class.isInstance(object)) {
			Predicate predicate = (Predicate) object;
			if (!predicate.identifier.equals(identifier)) {
				return false;
			}
			
			if (terms.length != predicate.terms.length) {
				return false;
			}
			
			for (int i=0; i<terms.length; i++) {
				if (!terms[i].equals(predicate.terms[i])) {
					return false;
				}
			}
			
			return true;
		}

		return false;
	}

	@Override
	public Predicate apply(Bindings bindings) {
		for (int i=0; i < terms.length; i++) {
//			System.out.println("\t handling: "+ terms[i]);
			if (terms[i] instanceof Variable) {
				Variable variable = (Variable) terms[i];
				if (variable.isFree()) {
					ITerm value = bindings.getStoredValue(variable);
//					System.out.println("\t\t assigning value: "+ value);
					if (value != null) {
						try {
							variable.assign(value);
						} catch (TypeException e) {
							// TODO Auto-generated catch block
							e.printStackTrace();
						}
					}
				} else {
					terms[i] = variable.value();
				}
			} else {
				terms[i].apply(bindings);
			}
		}
		return this;
	}

	@Override
	public Predicate copy() {
		ITerm[] trms = new ITerm[terms.length];
		for (int i=0; i<terms.length; i++) {
			trms[i] = terms[i].copy();
		}
		return new Predicate(identifier, trms);
	}
	
	@Override
	public Predicate copy(Map<String, Variable> vars) {
		ITerm[] trms = new ITerm[terms.length];
		for (int i=0; i<terms.length; i++) {
			if (terms[i] instanceof Variable) {
				Variable variable = vars.get(((Variable) terms[i]).identifier());
				if (variable == null) {
					variable = (Variable) terms[i].copy();
//					System.out.println("[Predicate] Adding variable: " + variable);
					vars.put(variable.identifier(), variable);
				}
				trms[i] = variable;
			} else {
//				System.out.println("[Predicate] Copying: " + terms[i]);
				trms[i] = terms[i].copy(vars);
			}
		}
		return new Predicate(identifier, trms);
	}

	public String signature() {
		return signature;
	}

	public boolean matches(Predicate id) {
		if (!identifier.equals(id.identifier)) return false;
		
		for (int i=0; i<terms.length; i++) {
			if (!terms[i].type().equals(id.terms[i].type())) return false;
		}
		return true;
	}

	public boolean hasFreeVariables() {
		for (ITerm term : terms) {
			if (term.hasFreeVariables()) return true;
		}
		return false;
	}
	
	@Override
	public Object accept(ILogicVisitor visitor) {
		return visitor.visit(this);
	}
}
